YES(O(1),O(n^3))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []()))
  , shuffle([]()) -> []()
  , shuffle(::(x, xs)) -> ::(x, shuffle(rev(xs))) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^3))

The input is overlay and right-linear. Switching to innermost
rewriting.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []()))
  , shuffle([]()) -> []()
  , shuffle(::(x, xs)) -> ::(x, shuffle(rev(xs))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We add following dependency tuples:

Strict DPs:
  { @^#([](), ys) -> c_1()
  , @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#([]()) -> c_3()
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#([]()) -> c_5()
  , shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
  { @^#([](), ys) -> c_1()
  , @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#([]()) -> c_3()
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#([]()) -> c_5()
  , shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []()))
  , shuffle([]()) -> []()
  , shuffle(::(x, xs)) -> ::(x, shuffle(rev(xs))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We estimate the number of application of {1,3,5} by applications of
Pre({1,3,5}) = {2,4,6}. Here rules are labeled as follows:

  DPs:
    { 1: @^#([](), ys) -> c_1()
    , 2: @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
    , 3: rev^#([]()) -> c_3()
    , 4: rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
    , 5: shuffle^#([]()) -> c_5()
    , 6: shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
Weak DPs:
  { @^#([](), ys) -> c_1()
  , rev^#([]()) -> c_3()
  , shuffle^#([]()) -> c_5() }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []()))
  , shuffle([]()) -> []()
  , shuffle(::(x, xs)) -> ::(x, shuffle(rev(xs))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ @^#([](), ys) -> c_1()
, rev^#([]()) -> c_3()
, shuffle^#([]()) -> c_5() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []()))
  , shuffle([]()) -> []()
  , shuffle(::(x, xs)) -> ::(x, shuffle(rev(xs))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { @([](), ys) -> ys
    , @(::(x, xs), ys) -> ::(x, @(xs, ys))
    , rev([]()) -> []()
    , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We decompose the input problem according to the dependency graph
into the upper component

  { shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }

and lower component

  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs)) }

Further, following extension rules are added to the lower
component.

{ shuffle^#(::(x, xs)) -> rev^#(xs)
, shuffle^#(::(x, xs)) -> shuffle^#(rev(xs)) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
  Weak Trs:
    { @([](), ys) -> ys
    , @(::(x, xs), ys) -> ::(x, @(xs, ys))
    , rev([]()) -> []()
    , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  Due to missing edges in the dependency-graph, the right-hand sides
  of following rules could be simplified:
  
    { shuffle^#(::(x, xs)) -> c_6(shuffle^#(rev(xs)), rev^#(xs)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs: { shuffle^#(::(x, xs)) -> c_1(shuffle^#(rev(xs))) }
  Weak Trs:
    { @([](), ys) -> ys
    , @(::(x, xs), ys) -> ::(x, @(xs, ys))
    , rev([]()) -> []()
    , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We use the processor 'matrix interpretation of dimension 1' to
  orient following rules strictly.
  
  DPs:
    { 1: shuffle^#(::(x, xs)) -> c_1(shuffle^#(rev(xs))) }
  
  Sub-proof:
  ----------
    The following argument positions are usable:
      Uargs(c_1) = {1}
    
    TcT has computed following constructor-based matrix interpretation
    satisfying not(EDA).
    
                 [[]] = [0]
                           
          [@](x1, x2) = [1] x1 + [1] x2 + [0]
                                             
         [::](x1, x2) = [1] x1 + [1] x2 + [1]
                                             
            [rev](x1) = [1] x1 + [0]
                                    
          [rev^#](x1) = [1] x1 + [0]
                                    
      [shuffle^#](x1) = [1] x1 + [1]
                                    
        [c_6](x1, x2) = [1] x1 + [1] x2 + [0]
                                             
                  [c] = [0]
                           
            [c_1](x1) = [1] x1 + [0]
    
    This order satisfies following ordering constraints
    
               [@([](), ys)] =  [1] ys + [0]                 
                             >= [1] ys + [0]                 
                             =  [ys]                         
                                                             
          [@(::(x, xs), ys)] =  [1] x + [1] xs + [1] ys + [1]
                             >= [1] x + [1] xs + [1] ys + [1]
                             =  [::(x, @(xs, ys))]           
                                                             
                 [rev([]())] =  [0]                          
                             >= [0]                          
                             =  [[]()]                       
                                                             
            [rev(::(x, xs))] =  [1] x + [1] xs + [1]         
                             >= [1] x + [1] xs + [1]         
                             =  [@(rev(xs), ::(x, []()))]    
                                                             
      [shuffle^#(::(x, xs))] =  [1] x + [1] xs + [2]         
                             >  [1] xs + [1]                 
                             =  [c_1(shuffle^#(rev(xs)))]    
                                                             
  
  The strictly oriented rules are moved into the corresponding weak
  component(s).
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak DPs: { shuffle^#(::(x, xs)) -> c_1(shuffle^#(rev(xs))) }
  Weak Trs:
    { @([](), ys) -> ys
    , @(::(x, xs), ys) -> ::(x, @(xs, ys))
    , rev([]()) -> []()
    , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  The following weak DPs constitute a sub-graph of the DG that is
  closed under successors. The DPs are removed.
  
  { shuffle^#(::(x, xs)) -> c_1(shuffle^#(rev(xs))) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { @([](), ys) -> ys
    , @(::(x, xs), ys) -> ::(x, @(xs, ys))
    , rev([]()) -> []()
    , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  No rule is usable, rules are removed from the input problem.
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Rules: Empty
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  Empty rules are trivially bounded

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs)) }
Weak DPs:
  { shuffle^#(::(x, xs)) -> rev^#(xs)
  , shuffle^#(::(x, xs)) -> shuffle^#(rev(xs)) }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

DPs:
  { 1: @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , 2: rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , 3: shuffle^#(::(x, xs)) -> rev^#(xs)
  , 4: shuffle^#(::(x, xs)) -> shuffle^#(rev(xs)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_2) = {1}, Uargs(c_4) = {1, 2}
  TcT has computed following constructor-restricted polynomial
  interpretation.
           [[]]() = 0            
                                 
      [@](x1, x2) = x1 + x2      
                                 
     [::](x1, x2) = 1 + x2       
                                 
        [rev](x1) = x1           
                                 
    [@^#](x1, x2) = x1 + x1*x2   
                                 
        [c_2](x1) = x1           
                                 
      [rev^#](x1) = x1^2         
                                 
    [c_4](x1, x2) = x1 + x2      
                                 
  [shuffle^#](x1) = 1 + x1 + x1^2
                                 
  
  This order satisfies following ordering constraints
  
             [@([](), ys)] =  ys                                         
                           >= ys                                         
                           =  [ys]                                       
                                                                         
        [@(::(x, xs), ys)] =  1 + xs + ys                                
                           >= 1 + xs + ys                                
                           =  [::(x, @(xs, ys))]                         
                                                                         
               [rev([]())] =                                             
                           >=                                            
                           =  [[]()]                                     
                                                                         
          [rev(::(x, xs))] =  1 + xs                                     
                           >= xs + 1                                     
                           =  [@(rev(xs), ::(x, []()))]                  
                                                                         
      [@^#(::(x, xs), ys)] =  1 + xs + ys + xs*ys                        
                           >  xs + xs*ys                                 
                           =  [c_2(@^#(xs, ys))]                         
                                                                         
        [rev^#(::(x, xs))] =  1 + 2*xs + xs^2                            
                           >  2*xs + xs^2                                
                           =  [c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))]
                                                                         
    [shuffle^#(::(x, xs))] =  3 + 3*xs + xs^2                            
                           >  xs^2                                       
                           =  [rev^#(xs)]                                
                                                                         
    [shuffle^#(::(x, xs))] =  3 + 3*xs + xs^2                            
                           >  1 + xs + xs^2                              
                           =  [shuffle^#(rev(xs))]                       
                                                                         

The strictly oriented rules are moved into the corresponding weak
component(s).

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
  { @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
  , rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
  , shuffle^#(::(x, xs)) -> rev^#(xs)
  , shuffle^#(::(x, xs)) -> shuffle^#(rev(xs)) }
Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ @^#(::(x, xs), ys) -> c_2(@^#(xs, ys))
, rev^#(::(x, xs)) -> c_4(@^#(rev(xs), ::(x, []())), rev^#(xs))
, shuffle^#(::(x, xs)) -> rev^#(xs)
, shuffle^#(::(x, xs)) -> shuffle^#(rev(xs)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { @([](), ys) -> ys
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , rev([]()) -> []()
  , rev(::(x, xs)) -> @(rev(xs), ::(x, []())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Wall-time: 44.494046s
CPU-time: 593.45778s

Hurray, we answered YES(O(1),O(n^3))